msg-spec-loc-decl(snd;i;da)
== k:Knd, l:IdLnk.
== <k,l>  dom(snd)  source(l) = i & (tgmap(p.1of(p);snd(<k,l>)). rcv(l,tg)  dom(da)) 

latex

---

clarification:

msg-spec-loc-decl(snd;i;da)
== k:Knd, l:IdLnk.
== fpf-dom(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq); <k,l>; snd)
==  source(l) = i  Id
==  & l_all(map(p.1of(p)
==  & l_all(map;fpf-ap(snd; product-deq(Knd;IdLnk;KindDeq;IdLnkDeq); <k,l>));Id;tg.fpf-dom
==  & (KindDeq; rcv(l,tg); da)) 

latex

Definitions	x:A. B(x), P  Q, P & Q, s = t, source(l), xL. P(x), map(f;as), x.A(x), 1of(t), f(x), product-deq(A;B;a;b), Knd, IdLnk, IdLnkDeq, <a,b>, Id, b, x  dom(f), KindDeq, rcv(l,tg)
FDL editor aliases	msg-spec-loc-decl